RCS "$Id: ModalityComplexProtected.sig,v 1.7 1998/08/13 11:38:52 pxs Exp $";
(* This is the signature used by "friend" modules that need to know *)
(* more about modalities than we want to tell the whole world *)
(* NB here, satisfies, filter raise Dunno if we can't tell. mentions says *)
(* false in such a case (i.e. gives benefit of doubt!) *)
signature MODALITY_COMPLEX_PROTECTED =
  sig

    structure A' : ACT
    datatype modality' = Modlist of A'.act list
    | Negmodlist of A'.act list
    | Modvar of V.var
    | Negmodvar of V.var

    include MODALITY_COMPLEX where A = A' where type modality = modality'

(* replace variables with what they denote in the global set environment*)
(* Raise Error if we find a variable not defined in the set env. *)
    val lookup: modality -> modality
(* these functions are only here for the translation from big to   *)
(* small logic   *)
    val justTau : modality
(* if modality's not an explicit list, do nothing *)
    val removeEps : modality -> modality
(* if modality's not an explicit list, complain! *)
    val addTau : modality -> modality
    val positive : modality -> bool
(* will say false if the modality's not an explicit list *)
    val mentionsEps : modality -> bool
  end
